| Definitions | State(ds), M.da(a), M.state, DeclaredType(ds;x), with declarations ds:dsda:daeffect of k(v) is x := f s v, f(x)?z, x : v, x : t initially x = v, M.ds(x), constant_function(f;A;B), f(x), A  B, A || B, Dsys, {T}, SQType(T), P   Q, P  Q, P  Q, R-discrete(R), Top, tt,  , Y, ff, reduce(f;k;as), deq-member(eq;x;L),  , mk-ma, only members of L read x, k sends only on links in L, k affects only members of L, (precondition a:Outcome(p) is P:State(ds) -> Bool), with declarations ds:dsda:dak(v) sends f s v on link l, only L sends on (l with tg), only members of L affect x :t, if b then t else f fi , , R-base-ma(R), R-loc(R), @i: A, , case(R)Rnone: noneleft right: comb(left;right)base(b). base(b), t.2, t.1, z != f(x) P(a;z), ma-ef-const(M;k;x;s;v), M(i), ma-init-const(M;x), P & Q,   x. t(x), t  T, [[R]], d-feasible-discrete(D;discrete), x dom(f),  b, P Q,  x:A. B(x), A ||+ B, f || g,  A,  , False, x(s), Unit, Realizer, State(ds), left right, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(),  |
| Lemmas | Knd sq, subtype rel self, fpf-cap-void-subtype, pi1 wf, pi2 wf, Kind-deq wf, fpf-cap-single1, Id sq, fpf-single-dom, fpf-single wf, ma-ef-const-join, ma-init-const-join, msga wf, d-feasible-discrete wf, m-sys-compatible wf, m-sys-join wf2, dsys wf, R-compat-implies, R-compat-symmetry, R-compat-discrete, bool sq, bool cases, fpf-join-ap, fpf-join-dom, R-Feasible-Rplus, R-Dsys-Rplus, not functionality wrt iff, assert of bnot, eqff to assert, assert-eq-id, eqtt to assert, iff transitivity, lsrc wf, not wf, bnot wf, eq id wf, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, R-Feasible wf, fpf-ap wf, top wf, fpf-trivial-subtype-top, Rnone wf, R-discrete wf, id-deq wf, product-deq wf, fpf-dom wf, assert wf, ma-st wf, R-Dsys wf, d-m wf, ma-da wf, false wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf |
Id